(set-logic QF_BV)
(declare-fun _substvar_47_ () (_ BitVec 1))
(declare-fun _substvar_48_ () (_ BitVec 3))
(declare-fun _substvar_49_ () (_ BitVec 1))
(declare-fun _substvar_50_ () (_ BitVec 3))
(declare-fun _substvar_51_ () (_ BitVec 1))
(declare-fun _substvar_52_ () (_ BitVec 1))
(declare-fun _substvar_53_ () (_ BitVec 16))
(declare-fun _substvar_54_ () (_ BitVec 16))
(declare-fun _substvar_55_ () (_ BitVec 16))
(declare-fun _substvar_56_ () (_ BitVec 16))
(declare-fun _substvar_57_ () (_ BitVec 16))
(declare-fun _substvar_58_ () (_ BitVec 16))
(declare-fun _substvar_59_ () (_ BitVec 16))
(declare-fun _substvar_60_ () (_ BitVec 1))
(declare-fun _substvar_62_ () (_ BitVec 1))
(declare-fun _substvar_63_ () (_ BitVec 3))
(declare-fun _substvar_64_ () (_ BitVec 1))
(declare-fun _substvar_65_ () (_ BitVec 1))
(declare-fun _substvar_66_ () (_ BitVec 16))
(declare-fun _substvar_67_ () (_ BitVec 16))
(declare-fun _substvar_68_ () (_ BitVec 3))
(declare-fun _substvar_69_ () (_ BitVec 1))
(declare-fun _substvar_115_ () (_ BitVec 16))
(declare-fun _substvar_141_ () (_ BitVec 1))
(declare-fun _substvar_142_ () (_ BitVec 1))
(declare-fun _substvar_148_ () (_ BitVec 1))
(declare-fun _substvar_155_ () (_ BitVec 16))
(declare-fun _substvar_160_ () (_ BitVec 1))
(declare-fun _substvar_166_ () (_ BitVec 1))
(declare-fun _substvar_167_ () (_ BitVec 1))
(declare-fun _substvar_169_ () (_ BitVec 16))
(declare-fun _substvar_172_ () (_ BitVec 1))
(declare-fun _substvar_368_ () Bool)
(declare-fun _substvar_375_ () Bool)
(declare-fun _substvar_396_ () Bool)
(assert (= _substvar_47_ (_ bv0 1)))
(assert (= _substvar_48_ (_ bv5 3)))
(assert (= _substvar_49_ (_ bv0 1)))
(assert (= _substvar_50_ (_ bv7 3)))
(assert _substvar_368_)
(assert (= _substvar_52_ _substvar_51_))
(assert (= _substvar_53_ (_ bv8 16)))
(assert (= _substvar_54_ (_ bv50825 16)))
(assert (= _substvar_55_ (_ bv0 16)))
(assert (= _substvar_56_ (_ bv611 16)))
(assert (= _substvar_57_ (_ bv705 16)))
(assert _substvar_375_)
(assert (= _substvar_59_ _substvar_58_))
(assert (= _substvar_62_ _substvar_60_))
(assert (= _substvar_63_ (_ bv3 3)))
(assert (= (_ bv0 1) _substvar_64_))
(assert (= _substvar_65_ (_ bv0 1)))
(assert (= _substvar_66_ (_ bv584 16)))
(assert (= _substvar_67_ (_ bv88 16)))
(assert (= _substvar_68_ (_ bv1 3)))
(assert (= _substvar_69_ (_ bv0 1)))
(assert (= _substvar_172_ (_ bv0 1)))
(assert (= (_ bv0 1) _substvar_166_))
(assert (= _substvar_142_ (_ bv0 1)))
(assert (= _substvar_141_ (_ bv0 1)))
(assert (= _substvar_148_ _substvar_160_))
(assert (let ((?x28741 (ite (or false (= _substvar_141_ (_ bv1 1)) (= _substvar_148_ (_ bv1 1))) (_ bv1 1) (_ bv0 1)))) (= _substvar_167_ ?x28741)))
(assert (= _substvar_169_ (ite _substvar_396_ _substvar_53_ _substvar_54_)))
(assert (= _substvar_155_ _substvar_56_))
(assert (= _substvar_115_ (ite (= _substvar_148_ (_ bv1 1)) _substvar_169_ _substvar_155_)))
(assert (= (_ bv0 16) (ite (= _substvar_167_ (_ bv1 1)) _substvar_115_ (_ bv0 16))))
(check-sat)
(exit)
